ma{-}interface{-}inl($X$) $\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$ma{-}interface{-}compose($\lambda$$x$.inl inl $x$  ;$X$)